
#include <math.h>
#include "dcdflib.H"
#include <stdlib.h>
#include <stdio.h>


int T = 100;




int main(int argc, char *argv[])

{

  //ALPHA BETA P0 P1 and BayesFactor definitions
  double ALPHA, BETA, P0, P1, BF;
  FILE *fp;
  int i,j;
  int status_cdf;
	
  //sucess and failure for the case of Walds algorithm and the Bayes Algorithm
  int success = 0;
  int failure = 0;
  int bsuccess = 0;
  int bfailure = 0;

  //output returned by the trace verification algorithm
  int out = -1;
	
  
  //file of the input model is called tcr_tomek%d.bngl where %d is count
  //input LTL file is called test%d.ltl where %d is countltl
  int count = 0, countltl = 0 ;
 

  char scount[100];
  char cmd[1000];
	
  //has a decision been reached yet?
  float decision = 0;
  float bayesdecision = 0;

  //was the wald's or bayes test complete
  int walddone=0;
  int bayesdone=0;

  //numerator being computes
  //bayes result being computed
  double nr=0;
  double bayesresult=0;


  /*beta function computation parameters with initial values*/
  int which = 1;
  double p = 0;
  double q = 0;
  double x = 0.4;
  double y = 1-x;
  double a = 20;
  double b = 10;
  double priora=1, priorb=1;
  int status = 1;
  double bound = 0;
  double betacdf=0;


  /*These lines test that the cdfbet library is producing correct results */
    cdfbet ( &which, &p, &q, &x, &y,  &a, &b, &status, &bound );
  //  printf ("%f %f\n",p,q);
	


    //compile the LTL translator

    printf("\n\nPlease wait...Assuring integrity of the Statistical Model Checker\n\n");
  system("./run > /dev/null");
	
  printf("\n\n BioLAB Statistical Model Checker\n Developer: Sumit Kumar Jha \n Carnegie Mellon University \n Experimental Software -- No Fitness for any Purpose Implied. Use at your own risk.\n\n");



  count=0;
  
	  
      walddone=0;
      bayesdone=0;

      count++;

      if(argc<9)
	{
	  printf("BioLab usage:\n ./BioLab  <model-file>  <property-file>  <Type-I error>  <Type-II error>  <Probability-Threshold>  <BayesFactor>   <Beta-Prior Shape Parameter 1>  <Beta-Prior Shape Parameter 2>\n");
	  exit(-1);
	}


      //read the inputs and parse them into variables
      ALPHA = atof(argv[3]);
      BETA = atof(argv[4]);
      P0 = atof(argv[5]);
      BF = atof(argv[6]);
      priora = atof(argv[7]);
      priorb = atof(argv[8]);
      


      while(1)
	{

	  //print model file
	  sprintf(cmd, "cp -rf %s ./bionetgen/BioNetGen_2.0.46/Models2/tcr_tomek1.bngl", argv[1]);
	  out = system(cmd);
	  if(out<0) exit(-1);

	  //execute model file using bionetgen
	  sprintf(scount,"%d",count);
	  sprintf(cmd,"./bionetgen/BioNetGen_2.0.46/Perl2/BNG2.pl ./bionetgen/BioNetGen_2.0.46/Models2/tcr_tomek%d.bngl  \n", count);	
	  out = system(cmd); 	
	  if(out<0) exit(-1);

	  //copy the data produced
	  sprintf(cmd,"cp -rf ./bionetgen/BioNetGen_2.0.46/Models2/tcr_tomek%d.gdat ./data.txt \n", count);	
	  out = system(cmd);
	  if(out<0) exit(-1);

 
	  //call analysis engine
	  sprintf(cmd,"./timedsimulate data.txt  \"%s\" > /dev/null \n",argv[2]);
	  out = system(cmd);


	  fp = fopen("decision","r");
	  if (fp==NULL)
	    {
	      printf("Sorry! The input TCTL formula may not be correct.\n");
	      while(1);
	    }
	  
	  fscanf(fp," %d ", &out);
	 
	  fclose(fp);  
	
	  if(out<0) exit(-1);
	
	  if (out!=0 && out !=1)
	    {
	      printf("\n\nAssertion Violation: TCTL property yielding %d which is neither 0 nor 1(256)\n",out);
	      exit(-1);	
	    }

	  if (out==0) 
	    failure++;
	  else
	    success++;

	  walddone=1;

	  /*Bayesian Decision Algorithm*/
	  which=1; p=-1; q=-1; a=success+priora; b=failure+priorb;
	  x=P0; y = 1-P0;
	  cdfbet ( &which, &p, &q, &x, &y, &a, &b, &status, &bound );
	  nr = p;
	  bayesdecision = (p/(1-p)); //*((1-P0)/P0);
	  if(p<0)
	    {
	      printf("Warning: Numerical issues detected on your platform! Change your probability-BF thresholds-priors: Status %d\n",status);
	      //bayesdecision=1;
	      exit(-1);
	    }

	  //report satisfaction
	  if (bayesdone ==0  && bayesdecision >= BF )
	    {
	      printf("\n\n Property %s Satisfied with probability less than %f\n\n",argv[2],P0); 
	      sprintf(cmd,"rm -rf bayesresult_%s_%f\n",argv[1],P0);
	      system(cmd);
	      sprintf(cmd,"echo  \"Satisfied Success %d Failure %d Bayes %f\" > bayesresult_%s_%f\n ",success, failure, bayesdecision,argv[1], P0);
	      system(cmd);
	      bayesdone=1;
	    }
	
	  //report failure
	  if (bayesdone ==0  && bayesdecision <= 1/BF )
	    {
	    
	      printf("\n\n Property %s *NOT* Satisfied with probability less than %f\n\n",argv[2],P0);  
	      sprintf(cmd,"rm -rf bayesresult_%s_%f\n",argv[1],P0);
	      system(cmd);
	      sprintf(cmd,"echo  \"NOT Satisfied Success %d Failure %d Bayes %f\" > bayesresult_%s_%f\n ",success, failure, bayesdecision,argv[1], P0);
	      system(cmd);
	      bayesdone=1;	     
	    }
	




	  if (walddone==1&&bayesdone==1) break;

	}
	

		
	
}

